作者：Dohan Kim
尽管几十年来，关于字符串上方程的推理已经得到了广泛的研究，但关于字符串上一般子句的等式推理的研究却很少。本文介绍了一种新的带字符串的叠加微积分，并提出了一个关于字符串上子句的等式定理证明框架。它为字符串上的分句提供了一个饱和过程，并证明了所提出的具有收缩规则的叠加演算是证明完备的。本文还提出了一个新的字符串上的单词问题的决策过程，w.r.t.如果在所提出的推理系统下r可以是有限饱和的，则字符串上的一组条件方程r。
Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition calculus with contraction rules is refutationally complete. This paper also presents a new decision procedure for word problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system.
论文链接：http://arxiv.org/pdf/2303.13257v1
更多计算机论文：http://cspaper.cn/